es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E. Dec(f2f+-pred(e',e)) 

latex

Definitions

P  Q, e c e', A, P  Q, P  Q, x(s), A c B, t  T, t.2, t.1, , P  Q, is_ack , x:A. B(x), is_req  , [e: i p j], P & Q, f2f+-pred(e',e), F2F+-decls, FIFO, x:A. B(x), Dec(P), False, [e: i p j]

Lemmas

decidable cand, decidable es-E-equal, decidable functionality, decidable not, decidable implies better, decidable rcv-it, decidable es-causl, decidable alle-causle, decidable existse-causle, event system wf, fifo wf, es-state wf, top wf, decidable wf, es-loc wf, bool wf, es-dtype wf, fifoC wf, Id wf, es-E wf, decidable snd-it, snd-it wf, decidable and, fifoR wf, rcv-it wf, not wf, es-causle wf, es-causl wf, fifoS wf, decidable or